Add complexity consistency audit; fix NonTautology, MinimumWeightDecoding and MaxCut<One> complexities - #1219

Agentic Review Report

PR #1219 at 81b4f236. Generic review: one audit example and two complexity-entry fixes with paper text.

Structural

• No generated exports (reduction_graph.json, problem_schemas.json, examples.json) in the diff. No unrelated edits, and no trait or macro changes.
• declare_variants! strings parse, and the MWD metadata test was updated. cargo test --lib -- minimum_weight_decoding non_tautology passes 29/29.
• NonTautology 2^num_vars: correct. Satisfiability -> NonTautology exists, so an unbounded-width DNF is CNF-SAT by De Morgan, and no O*((2-eps)^n) CNF-SAT algorithm is known. The old 1.307 came from 3-SAT and was wrong.
• MinimumWeightDecoding 2^num_cols: a valid upper bound, but not the best known. The new paper sentence is false; see finding 1.
• Audit soundness. Substituting upper-bound fields is sound in practice, but only because of the Growth trust contract (nonnegative, weakly monotone, subtraction widened to addition), not because "complexities are monotone". Non-monotone registered complexities such as (num_orientation_samples / num_links)^num_links land in Unknown and are skipped. ParameterTransform::compose already marks unsafe intermediate upper-bound substitutions unavailable. Today no unsound finding is emitted. The guard is implicit, though; see finding 3.

Quality

• The is_polynomial string heuristic is crude (finding 2). The polynomial bucket is empty today, so this is dormant.
• The audit is a report-only example with no regression test. That is acceptable for an example.

Feature test

• cargo run --release --example complexity_consistency_audit reproduces the PR body: 1935 paths, 420 consistent, 15 violating paths over 5 variants (SpinGlass, DecisionSpinGlass, GraphPartitioning via MaxCut/i64; MaximumSetPacking One/i64 via MIS), 100 incomparable, 1386 unknown, 14 uncomposable, and 0 polynomial findings.
• pred show NonTautology gives O(2^num_vars) and pred show MinimumWeightDecoding gives O(2^num_cols). pred create --example followed by pred solve reports optimal for both.

Findings

Important

1. docs/paper/reductions.typ:10968 and src/models/algebraic/minimum_weight_decoding.rs:182-184: the claim "In the worst case no algorithm is known beyond enumerating the solution coset" is false, and a trivial argument beats 2^m. Let r = rank(H). A consistent system has a solution of weight ≤ r: write s in a basis of r independent columns. So take the cheaper of two procedures:

   • enumerate the coset x0 + ker H, costing 2^(m-r);
   • enumerate all x with |x| ≤ r, costing sum_{w≤r} C(m,w) ≤ 2^(m·H(r/m)).

   The worst case is at 1 - ρ = H(ρ), ρ ≈ 0.2271, which gives O*(2^(0.7730 m)) for every instance.

   Fix: either register 2^(0.773 * num_cols) and state this derivation in the paper, or keep 2^num_cols and reword to something like "ISD exponents are average-case over random codes; we register the simple exhaustive bound O*(2^m), and better worst-case bounds follow from combining coset enumeration with low-weight enumeration." Also update the code comment ("no worst-case bound below exhaustive search over x is known") to match.

Minor
2. examples/complexity_consistency_audit.rs:78-85 (is_polynomial): this is a string heuristic over Expr::to_string().

• It classifies exp(n) and factorial(n) as polynomial, because neither contains a ^.
• It classifies n^(1/2) and n^(k) as exponential, because the exponent starts with (.
• The module doc (lines 10-11) says "both bounds polynomial", but only the registered side is checked.

Fix: decide from the growth domain instead. For example, add Growth::is_polynomial() (true iff no term has an exponential factor) in src/growth.rs and call it on registered_growth. Alternatively, drop the partition: it is empty today, and polynomial-vs-polynomial comparisons are already caveated.
3. examples/complexity_consistency_audit.rs:71-75: the comment "complexities are monotone" is not true for every registered string. Soundness actually rests on Growth::from_expr widening and its monotone trust contract.

Fix: make the guard explicit. Skip (count as unknown) when Growth::from_expr(&Expr::parse(target)) is Unknown before substituting, and reword the comment to cite the growth-domain contract.
4. examples/complexity_consistency_audit.rs:113-119: a variant with no registered complexity is counted as uncomposable, the same bucket as a transform-composition failure. Fix: use a separate counter (for example, missing complexity) so the coverage numbers in the PR body mean what they say.
5. examples/complexity_consistency_audit.rs:48: only Turing edges are filtered. An aggregate-only edge (witness == false) would yield a value bound, not a solution bound. None exist today (0 in reduction_graph.json). Fix: also continue when !edge.capabilities.witness, since the registered complexities describe witness-returning solves.
6. docs/paper/reductions.typ:5705: "the best known algorithm is O*(2^n) exhaustive search" overstates the case. For CNF-SAT with m = poly(n) clauses, 2^(n(1 - 1/O(log(m/n)))) algorithms exist (Calabro–Impagliazzo–Paturi). Fix: say "no O*((2-ε)^n) algorithm is known (SETH), so we register O*(2^n)."

Verdict: the NonTautology fix and the audit tool are sound. Finding 1 should be addressed before merge: the new MWD paper statement is mathematically false.

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 97.18%. Comparing base (a10ee83) to head (22b3c0b).

@@           Coverage Diff           @@
##             main    #1219   +/-   ##
=======================================
  Coverage   97.18%   97.18%           
=======================================
  Files        1146     1146           
  Lines      151076   151076           
=======================================
  Hits       146819   146819           
  Misses       4257     4257           

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

Addressed the Agentic Review Report in ea882aa:

1. Important, MinimumWeightDecoding bound: fixed. It now registers 2^(0.773 * num_cols), and the paper has the derivation. A consistent system has a solution of weight at most r = rank(H), so we can take the cheaper of coset enumeration, 2^(m−r), and weight-≤r enumeration, 2^(m·h(r/m)). The two balance at r/m ≈ 0.22709, giving an exponent of 0.77291, which 0.773 rounds up safely.
2. is_polynomial: removed, along with the polynomial/exponential split. The header now says a finding with a polynomial registered bound is only suggestive.
3. Monotonicity: paths whose target complexity the growth domain can't analyze are now skipped before substitution, and the comment now relies on the growth domain's monotone class.
4. Missing complexity: now has its own no complexity counter.
5. Aggregate-only edges: skipped (!capabilities.witness).
6. NonTautology wording: now "no O*((2−ε)^n) algorithm is known (SETH); we register O*(2^n)".

New audit result: 6 flagged variants. Fixing MinimumWeightDecoding exposed another stale entry, ThreeDimensionalMatching = 2^num_triples, which the 3DM → MWD reduction now bounds by 2^(0.773·num_triples). I've left that out of this PR, along with the MaxCut-weight and weighted-MIS items, as follow-ups.

Gates: make check passes except the pre-existing problemreductions-macros doctest (line 211, an ignore block forced by --include-ignored). make paper passes.

Please kindly check the following items (PR #1219):

• Paper (PDF): check the NonTautology and MinimumWeightDecoding complexity discussion (the 2^(0.773 m) derivation in particular)
• Implementation (Optional): spot-check examples/complexity_consistency_audit.rs and the two declare_variants! changes

Join the discussion on Zulip — feel free to ask questions or leave feedback there.

Retargeted onto feat/binary-ilp-to-sat (#1218) and merged that branch in (no rebase); the diff is again only this PR's five files. On the combined tree: cargo test --workspace, fmt, clippy, and make paper pass. The audit's totals now count the extra rules on #1218 (2155 paths: 431 consistent, 16 derived-better paths, 103 incomparable, 1594 unknown growth, 11 uncomposable); the flagged variants are the same six listed above (SpinGlass ×2 and GraphPartitioning via MaxCut weights, MaximumSetPacking ×2, ThreeDimensionalMatching). #1220 removes most of the unknown-growth bucket.